\begin{tabbing}
star{-}append($T$; $P$; $Q$)($L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=${\it LL}$:$T$ List List\+
\\[0ex]$\exists$${\it L'}$:$T$ List. (l\_all(${\it LL}$; ($T$ List); $X$.($P$($X$))) $\wedge$ ($Q$(${\it L'}$)) $\wedge$ ($L$ = append(concat(${\it LL}$); ${\it L'}$)))
\-
\end{tabbing}